ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), l:( List), A:ecl-trans-tuple{i:l}
ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), l:( List), A:ecl-trans-tuple(ds; da).
ecl-add-catch(A; l)  ecl-trans-tuple{i:l}(ds; da) 

latex

Definitions	t  T, , P  Q, False, A, A  B, , x:A. B(x), subtype(S; T), nat-deq, EqDecider(T), list-diff(eq; as; bs), ff, , bor(p; q), reduce(f; k; as), (i = j), band(p; q), deq-member(eq; x; L), b, ma-valtype(da; k), decl-state(ds), Knd, (x  l), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-add-catch(A; l), ecl-trans-tuple{i:l}(ds; da), Id, x. t(x), fpf(A; a.B(a)), filter(P; l)
Lemmas	filter wf, nat plus inc, ecl-trans-tuple wf, fpf wf, Id wf, l member wf, Knd wf, decl-state wf, ma-valtype wf, bnot wf, deq-member wf, band wf, eq int wf, reduce wf, bor wf, bool wf, bfalse wf, nat wf, list-diff wf, nat plus wf, nat-deq wf